\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl(${\it ds}$;${\it da}$), $k$:Knd, $l$:IdLnk, ${\it tg}$:Id, $n$:$\mathbb{N}$,\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$${\it da}$(rcv($l$,${\it tg}$))?Void), ${\it es}$:ES.
\-\\[0ex]source($l$) $=$ $i$
\\[0ex]$\Rightarrow$ (\=@$i$[[$A$;$k$ sends on $l$ with tag ${\it tg}$ [$s$,$v$.$f$($s$,$v$)], at marker $n$]]\+
\\[0ex]$\Leftrightarrow$
\\[0ex](\=es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)\+
\\[0ex]$\Rightarrow$ \=with decls \=${\it ds}$ \+\+
\\[0ex]${\it da}$
\-\\[0ex]sends on $l$ from $e$ 
\\[0ex]include \=if \=kind($e$) = $k$ $\wedge_{2}$ action[[$A$ $n$]][es{-}init(${\it es}$;$e$);$e$]$\rightarrow$\+\+
\\[0ex][$\langle$${\it tg}$$,\,$$f$((state when $e$),val($e$))$\rangle$]
\-\\[0ex]else nil fi 
\-\\[0ex]and only these for tags in [${\it tg}$]))
\-\-\-
\end{tabbing}